\begin{nusmvCommand}{check\_invar\_bmc\_inc}{Generates and solves the given 
invariant, or all invariants if no formula is given, using incremental algorithms}
 
\cmdLine{check\_invar\_bmc\_inc [-h | -n idx | -p "formula" [IN context]]
[-a algorithm]}

This command does the same thing as \code{check\_invar\_bmc} (see the
description on page \pageref{checkInvarBmcCommand}) but uses an
incremental algorithm and therefore usually runs considerably
quicker. The incremental algorithms exploit the fact that
satisfiability problems generated for a particular invariant have
common subparts, so information obtained during solving of one problem
can be used in solving another one. A SAT solver with an incremental
interface is required by this command. If no such SAT solver is
provided then this command will be unavailable.

There are two incremental algorithms which can be used: ``Dual'' and
``ZigZag''. Both algorithms are equally powerful, but may show
different performance depending on a SAT solver used and an invariant
being proved.  At the moment, the ``Dual'' algorithm cannot be used if
there are input variables in a given model. For additional information
about algorithms, consider \cite{een04temporal}.

Also, notice that during checking of invariants all the fairness
conditions associated with the model are ignored.

\begin{cmdOpt}

\opt{-n \parameter{\natnum{\it index}}} { {\it index} is the numeric index of a valid
INVAR specification formula actually located in the property
database.  The validity of {\it index} value is checked out by the
system.}
       
\opt{-p \parameter{"\anyexpr [IN context]"}}{ Checks the \anyexpr specified
on the command-line. \code{context} is the module instance name which
the variables in \anyexpr must be evaluated in.}
            
\opt{-k \parameter{\natnum{\it max\_length}}}{\natnum{\it max\_length}
is the maximum problem bound that can be reached. Only natural numbers
are valid values for this option. If no value is given the
environment variable \envvar{\it bmc\_length} is considered instead.}

\opt{-a \parameter{\natnum{\it alg}}}{\natnum{\it alg} specifies the
algorithm to use.  The value can be \code{dual} or
\code{zigzag}. If no value is given the environment variable
\envvar{\it bmc\_inc\_invar\_alg} is considered instead.}

\end{cmdOpt}

\end{nusmvCommand}
